\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$f$:(($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$), $L$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]($\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List). 
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\Rightarrow$ ($\uparrow$(ecl{-}trans{-}h($A$)(0,ecl{-}trans{-}state($A$; ${\it L'}$))))
\\[0ex]$\Rightarrow$ (${\it L'}$ = $L$))
\\[0ex]$\Rightarrow$ (\=ecl{-}trans{-}state(combine{-}ecl{-}tuples($A$; $B$; $f$; $g$); $L$)\+
\\[0ex]=
\\[0ex]$<$ecl{-}trans{-}state($A$; $L$), ecl{-}trans{-}state($B$; [])$>$
\\[0ex]$\in$ ecl{-}trans{-}type(combine{-}ecl{-}tuples($A$; $B$; $f$; $g$)))
\-
\end{tabbing}